An ongoing problem in the design of large systems is verifying that the system will behave in the manner intended by its designers. One approach has been to simply try out the system, either by building and testing the system itself or by building and testing a model of the system. Since there is no guarantee that an untested system will work as expected, building the system itself can be an expensive proposition. Thus, those skilled in the art have migrated toward building and testing a model of the system through software.
A system model can be said to be a computer program or block of code that, when executed, simulates the intended properties (i.e. functions and/or features) of the system. The computer program, or system model, is designed to accept inputs, perform functions and generate outputs in the same manner as would the actual system. Thus, by controlling the value of the system model inputs and monitoring the system model outputs, the functionality, or properties, of the system can be tested.
One method of testing a system model is called formal verification. In formal verification, the system model (i.e. computer program) is fed into a verification tool which converts the system model into a finite state machine. The finite state machine is a set of states and state transitions which mimic the operation of the system model in response to any given set of system model inputs. More specifically, each state represents a state or mode of operation the system model would enter given a set of inputs, and each state transition indicates the conditions (i.e. the value of system model inputs and system model variables) that must be met for the system model to transition from one state to another state.
Once a system model is converted to a state machine, a verification tool can test whether the system model behaves according to a set of expected behaviors (i.e. system properties). To do this, the verification tool varies the system model inputs and monitors which states the system model enters as a result of the inputs. This has been referred to as searching the state space of the system model. While searching the system model state space, the verification tool can check whether the system model enters a state or a cycle of states (i.e. repeatedly entering the same states over and over again) which the designers of the system define as "bad" or unintended. If the system model enters a "bad" state or a "bad" cycle of states, the system model is said to behave in a manner contradictory to that intended by the system designer, thus requiring a redesign.
Heretofore, in order to fully test every property of the system model through formal verification, the verification tool has had to run what is called a full search of the system model state space (i.e. the set of states and transitions that comprise the system model state machine). A full search of a system model state space is a test wherein, at each state, the system model inputs are varied such that they take on every value they can possibly assume in every possible order or sequence. That is, a full search tests the behavior of the system model in response to every possible set of input values that the system model inputs can possibly assume when the system model is in operation. As a result, a full search insures that the system model behavior is tested under every set of conditions that the system model can possibly undergo when in operation. Thus, a full search of a system model state space insures that every property of the system model is fully tested.
Looking at a simple example, a full search can be performed on a system model of a counter which increments a number, by one, up to ten each time it receives an input having a value of binary zero, and decrements the number, by one, down to zero each time it receives an input having a value of binary one. In such a system model, the numbers 0 through 10 represent the states the system model can enter, and the input values, binary zero and binary one, control the transitions between the states. As a result, the system model does not have or use any variables to define the behavior of the counter. Thus, this simple example is only intended to illustrate how the values (i.e. the sequence of values) input to the counter during a full search affect the behavior of the model of the counter (i.e. system model).
When fully searching the system model, the search engine of the verification tool can start at a state representing the number 1 (i.e. state 1), vary the input over the entire range of assumable values (i.e. binary one and binary zero) in every possible sequence (i.e. Sequence 1: binary zero, then binary one; Sequence 2: binary one, then binary zero), and identify the set of "next states" that the system model actually enters given each input in each sequence. For example, when inputting Sequence 1 (i.e. binary zero, then binary one) at state 1, the set of "next states are state 2 and state 0, respectively. And, when inputting Sequence 2 (i.e. binary one, then binary zero) at state 1, the set of "next states" are state 0 and state 1, respectively. Note, in this example, that the same set of "next states" (i.e. state 1 and state 0) are identified when inputting Sequence 1 as well as Sequence 2 to the system model at state 1.
For each of the identified "next states," the inputs are again varied over the entire range of possible values, in every possible sequence, to determine a new set of "next states." This process is repeated until the search engine traces through the system model state space and determines that the system model can only enter a state (i.e. next state) that was already entered, or checked. Ultimately, if the full search finds that the system model did not enter a "bad" state or set of states in response to a set of inputs, then the system model design is said to be error-free. That is, the system model is said to behave according to its design specification.
From this example, one can imagine that the more complex the system model becomes (i.e. the greater the number of system model inputs, the wider the range of assumable values for each input, and/or the greater the number of states), the greater the amount of computational resources that are necessary to complete a full search of the system model state space. In fact, it has been found that fully searching a sufficiently complex models with conventional verification tools can cause the verification tool to run out of computational resources (e.g. no more RAM available to the search engine). When this happens, the verification tool may "lock-up" (i.e. stop the full search) without providing the tester with data as to whether the system model had behaved as expected for any part of the full search performed before the "lock-up." As a result, when fully searching such complex system models with conventional verification tools, the tester may be left with no way of determining whether the system model has a design error (i.e. can enter a "bad" state or cycle of states).
One solution to this problem is to reduce the size of the system model and run a full search of the reduced model. That is, a tester or programmer experienced in the details of the system model (i.e. how the system inputs and system variables affect the behavior of the system model) may eliminate portions of the system model (i.e. lines of code and/or system model inputs and variables) that appear to have no effect on a limited set of system properties (i.e. those system functions which the programmer decides are not critical to check). This may require, however, substantial time, effort and experience on the part of the programmer to insure that the system model is not reduced such that the reduced model fails to retain those portions that are critical for testing the designated set of system properties. In addition, although reducing the system model reduces the amount of computational resources required to check the system model, such a reduction prevents a full search from checking the behavior of all system model properties.